(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 7))
(let ((e4 (+ v2 v2)))
(let ((e5 (/ e3 e3)))
(let ((e6 (/ e3 e3)))
(let ((e7 (* (- e3) e6)))
(let ((e8 (- e7 e5)))
(let ((e9 (- v1 e8)))
(let ((e10 (- e4 e5)))
(let ((e11 (- e4 v2)))
(let ((e12 (* e8 (- e3))))
(let ((e13 (/ e3 (- e3))))
(let ((e14 (- e6)))
(let ((e15 (- e9 e10)))
(let ((e16 (* e12 e11)))
(let ((e17 (- e11)))
(let ((e18 (* e15 e7)))
(let ((e19 (- e9)))
(let ((e20 (* e3 v1)))
(let ((e21 (- e19)))
(let ((e22 (+ e12 e21)))
(let ((e23 (+ e15 v0)))
(let ((e24 (>= v0 e20)))
(let ((e25 (< e13 e11)))
(let ((e26 (>= e10 e15)))
(let ((e27 (> e23 e18)))
(let ((e28 (> e23 e21)))
(let ((e29 (= v1 e4)))
(let ((e30 (= e4 e10)))
(let ((e31 (distinct e9 e14)))
(let ((e32 (> e5 e22)))
(let ((e33 (< e9 e4)))
(let ((e34 (> e9 e13)))
(let ((e35 (> e9 e6)))
(let ((e36 (<= v1 e7)))
(let ((e37 (>= e9 e10)))
(let ((e38 (> e22 e12)))
(let ((e39 (= v1 v0)))
(let ((e40 (<= e16 e12)))
(let ((e41 (distinct e10 e9)))
(let ((e42 (distinct e12 e23)))
(let ((e43 (= e23 e10)))
(let ((e44 (< e12 v2)))
(let ((e45 (< e19 e11)))
(let ((e46 (> e7 e10)))
(let ((e47 (>= e12 e21)))
(let ((e48 (> e12 e17)))
(let ((e49 (= v2 e22)))
(let ((e50 (< e10 e15)))
(let ((e51 (< e6 e8)))
(let ((e52 (= e13 e20)))
(let ((e53 (<= e19 e18)))
(let ((e54 (distinct e4 e11)))
(let ((e55 (< e5 e9)))
(let ((e56 (< e7 e6)))
(let ((e57 (> e12 e15)))
(let ((e58 (>= e22 e14)))
(let ((e59 (> e10 v2)))
(let ((e60 (distinct e12 e8)))
(let ((e61 (= e5 e14)))
(let ((e62 (distinct e13 e17)))
(let ((e63 (< e18 v2)))
(let ((e64 (>= e10 e12)))
(let ((e65 (distinct e14 v1)))
(let ((e66 (< e10 e9)))
(let ((e67 (>= e14 e12)))
(let ((e68 (> e12 e5)))
(let ((e69 (> e5 e6)))
(let ((e70 (<= v1 v0)))
(let ((e71 (> e11 e8)))
(let ((e72 (> e20 e8)))
(let ((e73 (<= e19 e13)))
(let ((e74 (>= e12 e15)))
(let ((e75 (distinct e6 e10)))
(let ((e76 (<= e9 e22)))
(let ((e77 (= e11 e16)))
(let ((e78 (< e4 e16)))
(let ((e79 (<= v2 e20)))
(let ((e80 (>= e8 e11)))
(let ((e81 (distinct e13 e9)))
(let ((e82 (> e6 e6)))
(let ((e83 (>= e21 v2)))
(let ((e84 (distinct e23 e12)))
(let ((e85 (and e58 e58)))
(let ((e86 (and e78 e63)))
(let ((e87 (or e59 e79)))
(let ((e88 (not e61)))
(let ((e89 (=> e34 e69)))
(let ((e90 (xor e30 e89)))
(let ((e91 (not e68)))
(let ((e92 (ite e49 e29 e70)))
(let ((e93 (and e85 e41)))
(let ((e94 (and e35 e24)))
(let ((e95 (=> e88 e90)))
(let ((e96 (=> e91 e81)))
(let ((e97 (= e45 e26)))
(let ((e98 (not e62)))
(let ((e99 (=> e65 e44)))
(let ((e100 (not e75)))
(let ((e101 (and e80 e97)))
(let ((e102 (or e99 e50)))
(let ((e103 (= e83 e64)))
(let ((e104 (not e67)))
(let ((e105 (ite e96 e71 e46)))
(let ((e106 (or e77 e100)))
(let ((e107 (ite e48 e43 e103)))
(let ((e108 (= e93 e38)))
(let ((e109 (ite e92 e27 e72)))
(let ((e110 (= e108 e102)))
(let ((e111 (or e28 e40)))
(let ((e112 (= e25 e110)))
(let ((e113 (ite e104 e94 e31)))
(let ((e114 (= e74 e105)))
(let ((e115 (xor e114 e37)))
(let ((e116 (=> e51 e32)))
(let ((e117 (or e86 e73)))
(let ((e118 (and e82 e76)))
(let ((e119 (and e60 e117)))
(let ((e120 (= e116 e118)))
(let ((e121 (=> e47 e39)))
(let ((e122 (and e98 e87)))
(let ((e123 (and e115 e54)))
(let ((e124 (=> e106 e52)))
(let ((e125 (or e36 e84)))
(let ((e126 (not e123)))
(let ((e127 (not e125)))
(let ((e128 (xor e107 e112)))
(let ((e129 (or e56 e53)))
(let ((e130 (not e126)))
(let ((e131 (or e66 e66)))
(let ((e132 (= e33 e131)))
(let ((e133 (=> e95 e101)))
(let ((e134 (= e127 e113)))
(let ((e135 (xor e134 e42)))
(let ((e136 (xor e121 e121)))
(let ((e137 (and e133 e128)))
(let ((e138 (=> e55 e129)))
(let ((e139 (xor e57 e130)))
(let ((e140 (or e124 e124)))
(let ((e141 (ite e135 e132 e109)))
(let ((e142 (and e111 e138)))
(let ((e143 (and e137 e140)))
(let ((e144 (xor e122 e120)))
(let ((e145 (or e136 e142)))
(let ((e146 (= e139 e141)))
(let ((e147 (=> e144 e146)))
(let ((e148 (not e145)))
(let ((e149 (and e148 e119)))
(let ((e150 (and e149 e149)))
(let ((e151 (and e150 e147)))
(let ((e152 (and e143 e143)))
(let ((e153 (xor e151 e151)))
(let ((e154 (= e153 e153)))
(let ((e155 (= e152 e154)))
e155
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
